(**************************************************************************)
(*                                                                        *)
(*                                  Cubicle                               *)
(*             Combining model checking algorithms and SMT solvers        *)
(*                                                                        *)
(*                  Sylvain Conchon and Alain Mebsout                     *)
(*                  Universite Paris-Sud 11                               *)
(*                                                                        *)
(*  Copyright 2011. This file is distributed under the terms of the       *)
(*  Apache Software License version 2.0                                   *)
(*                                                                        *)
(**************************************************************************)

(* open Options *)

exception ReachBound

type op_comp = Eq | Lt | Le | Neq
type op_arith = Plus | Minus

type sort = Glob | Arr | Constr | Var

type const = ConstInt of Num.num | ConstReal of Num.num | ConstName of string

let compare_const c1 c2 = match c1, c2 with
  | (ConstInt n1 | ConstReal n1), (ConstInt n2 | ConstReal n2) ->
      Num.compare_num n1 n2
  | (ConstInt _ | ConstReal _), _ -> -1
  | _, (ConstInt _ | ConstReal _) -> 1
  | ConstName h1, ConstName h2 -> String.compare h1 h2

module MConst = struct 
  module M = Map.Make (struct type t = const let compare = compare_const end)
  include M

  exception Choose of const * int
  let choose m =
    try
      M.iter (fun c i -> raise (Choose (c, i))) m;
      raise Not_found
    with Choose (c, i) -> c, i

end

let compare_constants = MConst.compare Pervasives.compare 

type term = 
  | Const of const
  | Elem of string * sort
  | Access of string * string list
  | Arith of term * const

(* let rec compare_term t1 t2 =  *)
(*   match t1, t2 with *)
(*     | Const c1, Const c2 -> compare_constants c1 c2 *)
(*     | Const _, _ -> -1 | _, Const _ -> 1 *)
(*     | Elem (s1, _), Elem (s2, _) -> String.compare s1 s2 *)
(*     | Elem _, _ -> -1 | _, Elem _ -> 1 *)
(*     | Access (a1, i1, _), Access (a2, i2, _) -> *)
(* 	let c = String.compare a1 a2 in *)
(* 	if c<>0 then c else String.compare i1 i2 *)
(*     | Access _, _ -> -1 | _, Access _ -> 1  *)
(*     | Arith (t1, _, cs1), Arith (t2, _, cs2) -> *)
(* 	let c = String.compare t1 t2 in *)
(* 	if c<>0 then c else compare_constants cs1 cs2 *)

type acc_eq = { a : string; i: string; e: term }

module rec Atom : sig
  type t =
    | True
    | False
    | Comp of term * op_comp * term                                        
    | Ite of SAtom.t * t * t

  val compare : t -> t -> int

end = struct
  
  type t =
    | True
    | False
    | Comp of term * op_comp * term
    | Ite of SAtom.t * t * t

  let rec compare a1 a2 = assert false 
    (* match a1, a2 with *)
    (*   | True, True -> 0 *)
    (*   | True, _ -> -1 | _, True -> 1 *)
    (*   | False, False -> 0 *)
    (*   | False, _ -> -1 | _, False -> 1 *)
    (*   | Comp (x1, op1, y1), Comp (x2, op2, y2) -> *)
    (*       let c1 = compare_term x1 x2 in *)
    (*       if c1 <> 0  then c1  *)
    (*       else  *)
    (*         let c0 = Pervasives.compare op1 op2 in *)
    (*         if c0 <> 0 then c0  *)
    (*         else  *)
    (*           let c2 = compare_term y1 y2 in c2 *)
    (*   | Comp _, _ -> -1 | _, Comp _ -> 1 *)
    (*   | Ite (sa1, a1, b1), Ite (sa2, a2, b2) -> *)
    (*       let c = SAtom.compare sa1 sa2 in *)
    (*       if c<>0 then c else  *)
    (*         let c = compare a1 a2 in *)
    (*         if c<>0 then c else compare b1 b2 *)

end
and SAtom : Set.S with type elt = Atom.t = Set.Make(Atom)


open Atom


type update = {
  up_arr : string;
  up_arg : string list;
  up_swts : (SAtom.t * term) list;
}

type action = Aassign of string * term | Aupd of update | Anondet of string
    
type transition = {
  tr_name : string;
  tr_args : string list;
  tr_reqs : SAtom.t;
  tr_ureq : (string * SAtom.t list) list;
  tr_assigns : (string * term) list;
  tr_upds : update list;
  tr_nondets : string list
}

type elem = string * (string list)



type decl = Dglobal of string * string | Dconst of string * string
            | Darray of string * (string list * string)



type decls =
    | Dlist of decl list
    | Dapp of decls * decls

let nop = Dlist []

let decl_l l = Dlist l

let (++) c1 c2 = Dapp (c1, c2)
                
type system = {
  type_defs : elem list;
  decls : decls;
  init : string option * SAtom.t;
  invs : (string list * SAtom.t) list;
  cands : (string list);
  unsafe : (string list * SAtom.t) list;
  forward : (string list * string list * SAtom.t) list;
  trans : transition list
}
    


    
(* Pretty-printer *)

open Format 

let rec print_sep_elmt sep fmt f = function
| [] -> ()
| [e] -> fprintf fmt "%a" f e
| s::t -> begin fprintf fmt "%a%s" f s sep; print_sep_elmt sep fmt f t end

let print_op_comp fmt = function
  | Eq -> fprintf fmt "="
  | Lt -> fprintf fmt "<"
  | Le -> fprintf fmt "<="
  | Neq -> fprintf fmt "<>"

let print_const fmt = function
  | ConstInt n -> fprintf fmt "%s" (Num.string_of_num n)
  | ConstReal n -> fprintf fmt "%s" (Num.string_of_num n)
  | ConstName s -> fprintf fmt "%s" s

let rec print_term fmt = function
  | Const c -> print_const fmt c
  | Elem (str, srt) -> fprintf fmt "%s" str
  | Access (str, strl) -> fprintf fmt "%s[" str;
        print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) strl;
        fprintf fmt "]"
  | Arith (term, cst) -> fprintf fmt "%a + %a" print_term term print_const cst
  (* Attention, signe +/- *)

let rec print_atom fmt = function
  | True -> fprintf fmt "True"
  | False -> fprintf fmt "False"
  | Comp (t1, op, t2) -> fprintf fmt "%a %a %a"
      print_term t1 print_op_comp op print_term t2
  | Ite (sa, a1, a2) -> fprintf fmt "ite %a %a %a"
      print_satom sa print_atom a1 print_atom a2
(* Je ne vois pas à quoi ça correspond *)

and print_satom fmt sa =
  print_sep_elmt " && " fmt print_atom (SAtom.elements sa) 
    
let print_update fmt u =
  fprintf fmt "%s [" u.up_arr;
  print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) u.up_arg;
  fprintf fmt "] := case\n";
  print_sep_elmt "\n" fmt (fun fmt (atoms, term) ->
    fprintf fmt "| %a : %a" print_satom atoms print_term term 
  ) u.up_swts

(*    
let print_action fmt = function
  | Aassign (s, term) -> fprintf fmt "%s := %a\n" s print_term term
  | Aupd u -> print_update fmt u 
  | Anondet s -> fprintf fmt "%s := .\n" s
*)

let print_assigns fmt assign =
  let str, term = assign in
  fprintf fmt "%s := %a\n" str print_term term

let print_uliteral fmt ulit = 
  let ident, satoms = ulit in
  fprintf fmt "forall_other %s . (\n" ident;
  print_sep_elmt " || " fmt print_satom satoms;
  fprintf fmt "\n)\n"
    
let print_transition fmt tr =
  fprintf fmt "transition %s " tr.tr_name;
  print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s) tr.tr_args; 
  fprintf fmt " requires {\n";
  print_satom fmt tr.tr_reqs ;
  if (not (SAtom.is_empty tr.tr_reqs) || (tr.tr_ureq != [])) then 
  fprintf fmt "\n&&\n";
  List.iter (print_uliteral fmt) tr.tr_ureq;
  fprintf fmt "\n}\n";
  fprintf fmt "{\n";
(*  List.iter (print_action fmt) tr.tr_actions;*)
  List.iter (print_assigns fmt) tr.tr_assigns;
  List.iter (print_update fmt) tr.tr_upds;
  List.iter (fprintf fmt "%s := .\n") tr.tr_nondets;
  fprintf fmt "\n}\n"

let print_invs fmt invs =
  List.iter (fun inv ->
    let ids, cube = inv in 
    fprintf fmt "invariant (";
    print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s) ids;
    fprintf fmt ") {\n%a\n}\n" print_satom cube
  ) invs

let print_elem fmt elem =
  let id, constr = elem in 
  fprintf fmt "type %s = " id;
  print_sep_elmt " | " fmt (fun fmt s -> fprintf fmt "%s" s) constr

let print_typedef fmt type_defs =
  print_sep_elmt "\n" fmt print_elem type_defs;
  fprintf fmt "\n"

let print_unsafe fmt (sl, sa) =
  fprintf fmt "unsafe (%a) {\n%a\n}\n"
    (fun fmt -> print_sep_elmt " " fmt (fun fmt s -> fprintf fmt "%s" s))
    sl print_satom sa

let print_init fmt (p, sa) = (* optional proc, guard *)
  fprintf fmt "init (%s) {\n%a\n}\n"
    (match p with Some s -> s | None -> "") print_satom sa

let print_decl fmt = function
  | Dglobal (v, t) -> fprintf fmt "var %s : %s\n" v t
  | Dconst (c, t) -> fprintf fmt "const %s : %s\n" c t
  | Darray (a, (itl, ct)) -> fprintf fmt "array %s [" a;
        print_sep_elmt "," fmt (fun fmt s -> fprintf fmt "%s" s) itl;
        fprintf fmt "] : %s\n" ct

let rec print_decls fmt = function
    | Dlist l -> List.iter (print_decl fmt) l
    | Dapp (c1, c2) -> print_decls fmt c1; print_decls fmt c2
      
let print_system fmt system = 
  print_typedef fmt system.type_defs;
  (* List.iter (print_decl fmt) system.decls; *)
  print_decls fmt system.decls;
  print_init fmt system.init;
  print_invs fmt system.invs;
  List.iter (print_unsafe fmt) system.unsafe;
  List.iter (print_transition fmt) system.trans;
  
  














